functor Assem () : ASSEM =
struct
  structure T = Temp
  datatype reg = Eax | Ebp | Ebx | Ecx | Edi | Edx | Esi | Esp
  
  datatype st
    = Rf of int
    | Hp of int
    | Upd of st * exp * exp 
  and exp
    = IntNum of int 
    | Mem of int
    | Id of string 
    | Plus of exp * exp 
    | Minus of exp * exp
    | Times of exp * exp 
    | Sel of st * exp
    | Reg of reg
    | Zf
    | Sf

    | Some of exp
    | State of state
    | TrForm of string * exp
  
  and state 
    = S of {hp : st, rf : st}

  fun setSt {hp : st, rf : st}
    = S {hp = hp, rf = rf}

  datatype etype
    = Int
    | Ptr of etype
    | Str of string
    | Wild 

  fun getRf (state' : state) = 
      case state'
           of S state => #rf state

  fun getHp (state' : state) = 
      case state' 
           of S state => #hp state

  fun updRf (rf, state' : state) : state = 
      case state' 
       of S state => S {hp = #hp state, rf = rf}

  fun updHp (hp, state' : state) : state = 
      case state' 
       of S state => S {hp = hp, rf = #rf state}

  fun updSt ({hp, rf}, state' : state) : state = 
      case state'
       of S state => S {hp = hp, rf = rf}

  datatype prop 
    = True
    | Imply of prop * prop
    | Not of prop
    | And of prop * prop
    | Or of prop * prop
    | Gt of exp * exp
    | Ge of exp * exp
    | Lt of exp * exp
    | Le of exp * exp
    | Eq of exp * exp
    | Ne of exp * exp
    | Ex of (string * etype) * prop
    | Forall of (string * etype) * prop
    | Tree of st * exp * int * int * int 
    | List of st * exp * int * int 
    | InDomM of state * exp 
    | Pred of string * prop
    | GoodFrame of state * exp
    | Stack of state * state
    | NotInDomM of state * exp

  datatype aptr
    = Preg of reg
    | Pstk of int * reg
    | Pmem of int * aptr * pexp
    | Pgmem of int
    | Pid of string

  and pexp 
    = Pvar of aptr
    | PintNum of int
    | Pplus of pexp * pexp
    | Pminus of pexp * pexp
    | Ptimes of pexp * pexp

  datatype pprop
    = Ptrue
    | Pnot of pprop
    | Pand of pprop * pprop
    | Por of pprop * pprop
    | Pge of pexp * pexp
    | Pgt of pexp * pexp
    | Plt of pexp * pexp
    | Ple of pexp * pexp
    | Peq of pexp * pexp
    | Pne of pexp * pexp
    | Pforall of (string * etype) * pprop
    | Pex of (string * etype) * pprop
    | Pi of aptr list list
    | N of aptr list
    | D of aptr list
    | Ptree of pexp
    | Plist of pexp
    | Ppred of string * pprop
 
  type assert = state -> state ->  prop

  type lab = string

  datatype sec = Data | Other of string | Text


  type passert = pprop option

  type opta = int * ((assert * passert) option) 

  datatype instr
    = Addr of reg * reg
    | Addz of int * reg
    | Addm of int * reg * reg
    | Subr of reg * reg
    | Subz of int * reg
    | Subm of int * reg * reg
    | Mulr of reg * reg
    | Mulz of int * reg
    | Mulm of int * reg * reg
    | Div of reg

    | Movld of int * reg * reg
    | Movr of reg * reg
    | Movst of reg * int * reg
    | Movz of int * reg * etype

    | Xchg of reg * reg
    | Leab of int * reg * reg
    | Leal of lab * reg
    | Cmpr of reg * reg
    | Cmpz of int * reg
    | Pop of reg
    | Push of reg
    | Leave

    | Jg of lab * lab
    | Je of lab * lab
    | Jge of lab * lab
    | Jmp of lab
    | Call of lab * lab
    | Ret of lab

    | Section of sec
    | Label of string * opta
    | Directive of string
    | ExtrA of assert

    | Malloc of int * lab * etype
    | Free of reg

  datatype pf 
    = WfSeq of pf * string * (instr list)
   
    | WfJmp of string * instr 
    | WfJg of string * string * instr 
    | WfJe of string * string * instr
    | WfJge of string * string * instr
    | WfCall of string * string * instr
    | WfRet of string
    | WfMalloc of string * instr


  type codeblk = {label : string,
                  id : int,
                  code : instr list,
                  asst : (assert * passert) option,
                  wfpf : (pf * string) option,  
                  alist : (string * assert) list} 

  fun getCbPf (cb : codeblk) = #wfpf cb
  fun setCbPf (cb : codeblk, pf : pf, tag : string) =
      {label = #label cb, id = #id cb, code = #code cb, asst = #asst cb, wfpf = SOME (pf, tag), alist = #alist cb}
  fun getCbAlist (cb : codeblk) = #alist cb

  fun addCbAlist (cb : codeblk, apair : (string * assert)) =
      {label = #label cb, id = #id cb, code = #code cb, asst = #asst cb, wfpf = #wfpf cb, alist = (apair :: (#alist cb))}

  fun getCbFstA (cb : codeblk) = 
      let val alist = #alist cb
      in  case alist
           of  [] => raise Fail "alist is empty"
             | (a :: alist) => a
      end
  fun getCbLab (cb : codeblk)= #label cb
  fun getCbId (cb : codeblk) = #id cb
  fun getCbCode (cb : codeblk) = #code cb
  fun getCbAsst (cb : codeblk) = 
      let val a = #asst cb
      in  case a 
           of NONE => NONE
            | SOME (ass, pass) => SOME ass
      end
  fun setCbAsst (cb : codeblk, a : assert) =
      let val (ass, pass) = 
              case #asst cb
               of  NONE => (a, NONE)
                 | SOME (ass', pass') => (a, pass')
      in  {label = #label cb, id = #id cb, code = #code cb, asst = SOME (ass, pass), wfpf = #wfpf cb, alist = #alist cb}
      end

  fun getCbPasst (cb : codeblk) =
      let val a = #asst cb
      in  case a
           of NONE => NONE
            | SOME (ass, pass) => pass
      end

  fun getCbA (cb : codeblk) = #asst cb
  fun setCb (lab, id, code, asst, wfpf, alist) : codeblk = 
      {label = lab, id = id, code = code, asst = asst, wfpf = wfpf, alist = alist} 

  datatype arg
    = O of string
    | L of arg list
    | P of arg list
 
  datatype tactic
    = Tapply of string * ((string * string) list)
    | Tintros of (string list)
    | Tinversion_clear of string * (arg list)
    | Tproof
    | Tqed
    | Tauto
    | Tunfold of string
    | Tor of tactic * tactic
    | Tseq of tactic list
    | Tpara of (tactic list)
    | Tsplit
    | Texists of string
    | TexistsS of st * st
    | Trepeat of tactic
    | Tconstructor
    | Ttry of tactic
    | Tomega
    | TtacIn of tactic * string 
    | Tinduction of string * (arg list)
    | Tdestruct of string * (arg list)
    | Tsimpl
    | Tassert of string * prop
    | Tclear of string
    | Treflexivity
    | Treplace of exp * exp
    | Trewrite of string
    | Tinjection of string
    | Tcut of string


  type code4ptr = {label : string
                 , code : instr list
                 , asst : passert} 

  fun getCbLab4p (cb : code4ptr)= #label cb 
  fun getCbCode4p (cb : code4ptr) = #code cb
  fun getCbAsst4p (cb : code4ptr) = #asst cb
  fun setCb4p (lab, code, asst) = 
      {label = lab, code = code, asst = asst}

  type asmenv = (aptr * aptr * etype) list
  type asmsenv = (string * (int * etype) list) list
  fun lookupE0 (key, env) =
      case env
       of  [] => NONE
         | (x0, x1, t) :: xs => if x0 = key
                                then SOME t
                                else lookupE0 (key, xs)

  fun lookupE1 (key, env) =
      case env
       of  [] => NONE
         | (x0, x1, t) :: xs => if x1 = key
                                then SOME t
                                else lookupE1 (key, xs)
  fun lookupP0 (key, env) =
      case env
       of  [] => NONE
         | (x0, x1, t) :: xs => if x0 = key
                                then SOME x1
                                else lookupP0 (key, xs)

  fun lookupP1 (key, env) =
      case env
       of  [] => NONE
         | (x0, x1, t) :: xs => if x1 = key
                                then SOME x0
                                else lookupP1 (key, xs)
  fun lookupE (key, env) = 
      case env
       of [] => NONE
        | (x, t) :: xs => if x = key 
                          then SOME t
                          else lookupE (key, xs)
  fun lookup (key, env) =
      case env
       of [] => []
        | (x, e) :: xs => if x = key
                          then e
                          else lookup (key, xs)

  fun lookupS ((sname, offset), senv) = 
      let val fieldlist = lookupE (sname, senv)
      in  case fieldlist 
           of NONE => NONE
            | SOME fenv => lookupE (offset, fenv)
      end 

  type pprf = {f : string
             , p : passert
             , q : passert
             , prog : code4ptr list
             , env : asmenv}

  type ginf = {senv : asmsenv
             , data : instr list
	     , fRet : (string * etype) list}

  fun getFname (prf : pprf) = #f prf
  fun getCode (prf : pprf) = #prog prf
  fun getAsmEnv (prf : pprf) = #env prf
  fun getType (aptr, env : asmenv)=
      let val t1 = lookupE0 (aptr, env)
      in  case t1
           of  NONE => lookupE1 (aptr, env)
             | SOME t => SOME t
      end
  fun getOtherEnvPtr (aptr, env : asmenv) =
      let val p0 = lookupP0 (aptr, env)
          val p = case p0
                   of  NONE => lookupP1 (aptr, env)
                     | SOME p' => SOME p'
      in  case p
           of  NONE => raise Fail "no such pointer"
             | SOME p' => p'
      end
  fun getPre (prf : pprf) = #p prf
  fun getPost (prf : pprf) = #q prf
  fun setPprf (f : string, p: passert, q : passert, prog : code4ptr list, env : (aptr * aptr * etype) list) =
      {f = f, p = p, q = q, prog = prog, env = env}
  fun getParas (prfs : pprf list, callf : string) = 
      let fun mapEnv (Pstk(of1, Ebp), Pstk(of2, Esp), etp) = 
	      if of1 > 0 
	      then [(Pstk(of2, Esp), etp)]
	      else []
	    | mapEnv (Pgmem(of1), Pgmem(of2), etp) = []
	    | mapEnv _ = raise Fail "bug\n"

	  fun fdenv prf = 
	      if callf = (getFname prf)
	      then List.concat(List.map mapEnv (getAsmEnv prf))
	      else []
      in List.concat(List.map fdenv prfs)
      end

  fun getStrType ((s, off), inf : ginf) = lookupS ((s, off), #senv inf)
  fun getStrFields (s, inf : ginf) = lookup (s, #senv inf)
  fun getData (inf : ginf) = #data inf
  fun getFRet (fname, inf :ginf) = 
      let val fret = #fRet inf
	  fun fd i1 ((i2, tp)::r) = if i1 = i2
				    then tp
				    else (fd i1 r)
	    | fd i1 [] = raise Fail "cannot find return type\n"
      in fd fname fret
      end

  fun setGinf (senv : (string * (int * etype) list) list , data : instr list, fret : (string * etype) list) = 
      {senv = senv, data = data, fRet = fret}

  fun newAsst (asstopt : (assert * passert) option) : opta = (T.newNum (), asstopt)
  fun newAsstMain (asstopt : (assert * passert) option) : opta = (0, asstopt)
 
  fun getLabId (opta : opta) = (#1 opta)
  fun getLabA (opta : opta) = (#2 opta)
  fun getLabAsst (opta : opta) = 
      let val a = getLabA opta
      in  case a
           of NONE => NONE
            | SOME (ass, pass) => SOME ass
      end
  fun getLabPasst (opta : opta) =
      let val a = getLabA opta
      in  case a
           of NONE => NONE
            | SOME (ass, pass) => pass
      end

  fun itoString i = 
      if (i>=0)
      then Int.toString(i)
      else ("-"^(Int.toString(Int.abs(i))))

  fun sectoString Data = "\t.data"
    | sectoString Text = "\t.text"
    | sectoString (Other(s)) = "\t."^s

  fun rtoString r = 
      case r
       of Eax => "%eax"
        | Ebx => "%ebx"
        | Ecx => "%ecx"
        | Edx => "%edx"
        | Esi => "%esi"
        | Edi => "%edi"
        | Ebp => "%ebp"
        | Esp => "%esp"
  
  fun offtoString i = if i = 0 
                      then ""
                      else (itoString i)

  fun etype2str (Int) = "int"
    | etype2str (Ptr(tp)) = etype2str(tp)^"*"
    | etype2str (Str(stid)) = "struct "^stid
    | etype2str (Wild) = "wild"
    
  fun aptr2str ap = 
      let fun mtch (Preg(rg)) = rtoString rg
	    | mtch (Pstk(imm, rg)) = itoString(imm)^"("^rtoString(rg)^")"
	    | mtch (Pmem(imm, ap', Pvar(pe))) = aptr2str(ap')^"(->"^itoString(imm)^")"^pexp2str(Pvar(pe))
	    | mtch (Pmem(imm, ap', pe)) = if imm = 0
					  then "("^aptr2str(ap')^")"
					  else "("^aptr2str(ap')^"+"^itoString(imm)^")"
	    | mtch (Pgmem(imm)) = "G."^itoString(imm)
	    | mtch (Pid(str)) = str
      in mtch ap
      end
  and aptrs2str als = 
      (fn [] => "{}"
	| t => let val hder = List.hd(als)
		   val tler = List.tl(als)
		   val hder' = aptr2str hder
	       in "{"^String.concat(List.map (fn t => aptr2str(t)^", ") tler)^hder'^"}"
	       end) als
  
  and pexp2str pe = 
      let fun mtch (Pvar(ap)) = aptr2str ap
	    | mtch (PintNum(imm)) = itoString(imm)
	    | mtch (Pplus(pe1, pe2)) = (pexp2str(pe1))^" + "^(pexp2str(pe2))
	    | mtch (Pminus(pe1, pe2)) = (pexp2str(pe1))^" - "^(pexp2str(pe2))
	    | mtch (Ptimes(pe1, pe2)) = (pexp2str(pe1))^" * "^(pexp2str(pe2))
      in "("^(mtch pe)^")"
      end

  and pprop2str pp = 
      let fun mtch (Ptrue) = "true"
	    | mtch (Pnot(pp)) = "!"^(pprop2str pp)
	    | mtch (Pand(pp1, pp2)) = pprop2str(pp1)^" && "^pprop2str(pp2)
	    | mtch (Por(pp1, pp2)) = pprop2str(pp1)^" || "^pprop2str(pp2)
	    | mtch (Pge(pe1, pe2)) = pexp2str(pe1)^" >= "^pexp2str(pe2)
	    | mtch (Pgt(pe1, pe2)) = pexp2str(pe1)^" > "^pexp2str(pe2)
	    | mtch (Plt(pe1, pe2)) = pexp2str(pe1)^" < "^pexp2str(pe2)
	    | mtch (Ple(pe1, pe2)) = pexp2str(pe1)^" <= "^pexp2str(pe2)
	    | mtch (Peq(pe1, pe2)) = pexp2str(pe1)^" == "^pexp2str(pe2)
	    | mtch (Pne(pe1, pe2)) = pexp2str(pe1)^" != "^pexp2str(pe2)
	    | mtch (Pforall((str, et), pp')) = "forall "^str^" : "^(etype2str(et))^". "^pprop2str(pp')
	    | mtch (Pex((str, et), pp')) = "exists "^str^" : "^(etype2str(et))^". "^pprop2str(pp')
	    | mtch (Pi(als)) = 
	      (fn [] => "{}"
		| t => let val hder = List.hd(als)
			   val tler = List.tl(als)
			   val hder' = aptrs2str(hder)
		       in "("^String.concat(List.map (fn t => aptrs2str(t)^" && ") tler)^hder'^")"
		       end
	      ) als
	    | mtch (N(als)) = aptrs2str(als)^"N"
	    | mtch (D(als)) = aptrs2str(als)^"D"
	    | mtch (Ptree(pe)) = "tree"^(pexp2str(pe))
	    | mtch (Plist(pe)) = "list"^(pexp2str(pe))
	    | mtch (Ppred(str, pp')) = str^(pprop2str(pp'))
      in "("^(mtch pp)^")"
      end
  
  fun toString instr = 
      let fun t (Addr(r1, r2)) = "\taddl\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Addz(i, r)) = "\taddl\t$"^(itoString i)^", "^(rtoString r)^"\n"
            | t (Addm (i, r1, r2)) = "\taddl\t"^(offtoString i)^"("^(rtoString r1)^"), "^(rtoString r2)^"\n"
            | t (Subr(r1, r2)) = "\tsubl\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Subz(i, r)) = "\tsubl\t$"^(itoString i)^", "^(rtoString r)^"\n"
            | t (Subm (i, r1, r2)) = "\tsubl\t"^(offtoString i)^"("^(rtoString r1)^"), "^(rtoString r2)^"\n"
            | t (Mulr(r1,r2)) = "\timull\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Mulz (i,r)) = "\timull\t$"^(itoString i)^", "^(rtoString r)^"\n"
            | t (Mulm (i, r1, r2)) = "\timull\t"^(offtoString i)^"("^(rtoString r1)^"), "^(rtoString r2)^"\n"
            | t (Div r) = "\tcltd\n" ^ 
                          "\tidivl\t"^(rtoString r)^"\n"

            | t (Movr(r1,r2)) = "\tmovl\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Movz(i, r, t)) = "\tmovl\t$"^(itoString i)^", "^(rtoString r)^" #@ "^(etype2str t)^" #@\n"
            | t (Movld(i, r1, r2))= "\tmovl\t"^(offtoString i)^"("^(rtoString r1)^"), "^(rtoString r2)^"\n"
            | t (Movst(r1, i, r2)) = "\tmovl\t"^(rtoString r1)^", "^(offtoString i)^"("^(rtoString r2)^")\n"

            | t (Xchg (r1,r2)) = "\txchg\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Leal(l,r)) = "\tleal\t"^l^", "^(rtoString r)^"\n"
            | t (Leab(i, r1, r2)) = "\tleal\t"^(offtoString i)^"("^(rtoString r1)^"), "^(rtoString r2)^"\n"
            | t (Cmpr (r1, r2))= "\tcmpl\t"^(rtoString r1)^", "^(rtoString r2)^"\n"
            | t (Cmpz (i, r)) = "\tcmpl\t$"^(itoString i)^", "^(rtoString r)^"\n"
            | t (Push r) = "\tpushl\t"^(rtoString r)^"\n"
            | t (Pop r) = "\tpopl\t"^(rtoString r)^"\n"
            | t (Leave) = "\tleave\n"

            | t (Je (l, ln)) = "\tje\t"^l^"\n"
            | t (Jge (l, ln)) = "\tjge\t"^l^"\n"
            | t (Jg (l, ln)) = "\tjg\t"^l^"\n"
            | t (Jmp l) =  "\tjmp\t"^l^"\n"
            | t (Call (f, fret)) = (fn "print" => "\tcall\t"^f^"\n"
				     | "printb" => "\tcall\t"^f^"\n"
				     | "printp" => "\tcall\t"^f^"\n"
				     | _ => "\tsubl\t$4, %esp\n"^
					    "\tcall\t"^f^"\n"^
					    "\taddl\t$4, %esp\n"
				   ) f
            | t (Ret(l)) = "\tret\n"
 
            | t (Section sec) = "\n"^(sectoString sec)^"\n"
            | t (Label (l, opta)) =
	      let val p_passt = (fn NONE => ""
				  | SOME(t) => "#@ "^(pprop2str t)^"\n#@\n") (getLabPasst opta)
	      in l^":\n"^p_passt
	      end
            | t (Directive s) = s^"\n"
            | t (ExtrA a) = ""

            | t (Malloc (i, l, t)) = 
	      let val imul4 = i * 4;
	      in "\tmovl\t$"^(itoString imul4)^", %eax #@ int #@\n"^
                 "\tpushl\t%eax\n"^
		 "\tcall\tmalloc #@ "^(etype2str t)^" #@\n"^
                 "\taddl\t$4, %esp\n"
	      end
            | t (Free r) = "\tpushl\t"^(rtoString r)^"\n"^
                           "\tcall\tfree\n"^
                           "\taddl\t$4, %esp\n"
      in  t instr
      end

  fun asmenv2str aenvs = 
      let fun foreach (apt1, apt2, etp) = (aptr2str apt1)^" * "^(aptr2str apt2)^" : "^(etype2str etp)^"\n"
      in String.concat(List.map foreach aenvs)
      end

end
